Abstrakte Interpretation

Die abstrakte Interpretation ist eine Methode aus dem Bereich der Programmanalyse.

Ziel der abstrakten Interpretation ist es Informationen über das Verhalten von Programmen (Analyse der Semantik) zu bekommen, indem man von Teilen des Programms abstrahiert und die Anweisungen Schritt für Schritt nachvollzieht (Interpretation).

Bei der abstrakten Interpretation konzentriert man sich auf Teilaspekte der Ausführung der Anweisungen, man lässt einiges an Information geschickt weg (Abstraktion), erhält letztlich eine Näherung an die Programmsemantik, die aber für den gewünschten Zweck vollkommen ausreichen kann.

Viele Eigenschaften von Programmen sind nicht berechenbar, d. h. man kann kein Programm angeben, welches sie in endlicher Zeit mit endlichen Speicherressourcen für beliebige Programme berechnet. Durch eine Approximation, also das Weglassen von einigen Informationen, kann man zwar Fragen nach bestimmten Eigenschaften gar nicht mehr klären, dafür werden aber andere Eigenschaften in der vergröberten Sicht erst berechenbar.

Das Verfahren stammt von Radhia Cousot und Patrick Cousot.